#use "context.decls"

let list_nth : list -> nat -> nat |>
  { [] => ( 0 => 0
          | 1 => 0
          | 2 => 0
          | 3 => 0 )
  | [2] => ( 0 => 2
           | 1 => 0
           | 2 => 0
           | 3 => 0 )
  | [1; 2] => ( 0 => 1
              | 1 => 2
              | 2 => 0
              | 3 => 0 )
  | [1] => ( 0 => 1
           | 1 => 0
           | 2 => 0
           | 3 => 0 )
  | [2; 1] => ( 0 => 2
              | 1 => 1
              | 2 => 0
              | 3 => 0 )
  | [3; 2; 1] => ( 0 => 3
                 | 1 => 2
                 | 2 => 1
                 | 3 => 0 )
  } = ?
